Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:		f(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ f(a,f(b,f(a,f(a,f(b,f(a,f(a,f(a,f(b,x)))))))))

There are 9 dependency pairs:


2:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(a,f(b,f(a,f(a,f(b,f(a,f(a,f(a,f(b,x)))))))))
3:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(b,f(a,f(a,f(b,f(a,f(a,f(a,f(b,x))))))))
4:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(a,f(a,f(b,f(a,f(a,f(a,f(b,x)))))))
5:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(a,f(b,f(a,f(a,f(a,f(b,x))))))
6:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(b,f(a,f(a,f(a,f(b,x)))))
7:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(a,f(a,f(a,f(b,x))))
8:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(a,f(a,f(b,x)))
9:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(a,f(b,x))
10:		F(a,f(a,f(b,f(a,f(a,f(b,f(a,x)))))))	→ F(b,x)

The approximated dependency graph contains one SCC: {2,4,5,7-9}.

Consider the SCC {2,4,5,7-9}. By taking the AF π with π(f) = 1 and π(F) = 2 together with the lexicographic path order with precedence a ≻ b, the rules in {1,4,7,8} are weakly decreasing and the rules in {2,5,9} are strictly decreasing. There is one new SCC.
- Consider the SCC {4,7,8}. The constraints could not be solved.

Tyrolean Termination Tool (18.07 seconds) --- May 4, 2006